\part{数理逻辑}

\chapter{命题逻辑的基本概念}

\section{命题与连接词}

\begin{itementry}
    命题:非真即假的陈述句称为命题
\end{itementry}

\begin{itementry}
    真值:命题所表述的判断结果称为真值,真值只取真和假,任何命题的真值都是唯一的
\end{itementry}

\begin{itementry}
    真(假)命题:真值为真(假)的命题称为真(假)命题
    \begin{subentry}
        注:一般用小写英文字母表示命题,``1''表示真,``0''表示假
    \end{subentry}
\end{itementry}

\begin{itementry}
    简单命题(原子命题):不能被分解为更简单命题的命题成为原子命题
\end{itementry}

\begin{itementry}
    复合命题:由简单命题通过连接词联结而成的命题称为复合命题
\end{itementry}

\begin{itementry}
    悖论:既不能为真也不能为假的陈述句称为悖论,悖论不是命题
\end{itementry}

\begin{itementry}
    非:设\(p\)为命题,复合命题``非\(p\)''称为\(p\)的否定式,记为\(\neg p\),符号\(\neg\)称为否定联结词
\end{itementry}

\begin{itementry}
    且:设\(p,q\)是两个命题,复合命题``\(p\)并且\(q\)''称为\(p\)和\(q\)的合取式,记为\(p\wedge q\).\(\wedge\)称为合取联结词,规定\(p\wedge q\)为真当且仅当\(p,q\)同时为真
\end{itementry}

\begin{itementry}
    或:设\(p,q\)为两个命题,复合命题``\(p\)或\(q\)''称为\(p\)与\(q\)的析取式,记为\(p\vee q\),\(\vee\)称为析取联结词,规定\(p\vee q\)为假当且仅当\(p\)与\(q\)同时为假
\end{itementry}

\begin{itementry}
    蕴含:设\(p\),\(q\)为两个命题,复合命题``如果\(p\),则\(q\)''称为\(p\)与\(q\)的蕴含式,记为\(p\to q\),并称\(p\)为蕴含式的前件,\(q\)为蕴含式的后件.\(\to\)称为蕴含联结词.并规定\(p\to q\)为假当且仅当\(p\)为真\(q\)为假.\(p\to q\)的逻辑关系为\(q\)是\(p\)的必要条件
\end{itementry}

\begin{itementry}
    等价:设\(p,q\)为两个命题,复合命题``\(p\)当且仅当\(q\)''称为\(p\)与\(q\)的等价式,记为\(p\leftrightarrow q\),\(\leftrightarrow\)称为等价联结词.规定\(p\leftrightarrow q\)为真当且仅当\(p\)与\(q\)同时为真或同时为假.\(p\leftrightarrow q\)的逻辑关系为\(p\)与\(q\)互为充分必要条件
\end{itementry}

\begin{itementry}
    联结词的运算顺序:\((\hspace{0.5em}),\neg,\wedge,\vee,\to,\leftrightarrow\).对同一优先级,从左到右依次进行
\end{itementry}

\section{命题公式及其赋值}

\begin{itementry}
    命题常项/命题常元:真值确定的,不含变项的命题称为命题常项(或命题常元)
\end{itementry}

\begin{itementry}
    命题变项/命题变元:真值不确定的,含命题变项的命题称为命题变项(或命题变元)
\end{itementry}

\begin{itementry}
    合式公式/命题公式/命题形式/公式:
    \begin{theitem}
        \item 单个命题变项或命题常项是合式公式,并称为原子命题公式
        \item 若\(A\)是合式公式,则\(\neg A\)是合式公式
        \item 若\(A,B\)是合式公式,则\(A\wedge B,A\vee B,A\to B,A\leftrightarrow B\)是合式公式
        \item 有限次使用1-3形成的符号串是合式公式
    \end{theitem}
\end{itementry}

\begin{itementry}
    子公式:设\(A\)为合式公式,\(B\)为\(A\)中一部分,若\(B\)也是合式公式,则称\(B\)为\(A\)的子公式
\end{itementry}

\begin{itementry}
    公式层次:
    \begin{theitem}
        \item 若公式\(A\)是单个命题变项,则称\(A\)是\(0\)层公式
        \item 称\(A\)是\(n+1(n\geq 0)\)层公式当且仅当:
        \begin{theitem}
            \item[(1)] \(A=\neg B\),\(B\)是\(n\)层公式
            \item[(2)] \(A=B\wedge C\),其中\(B,C\)分别为\(i\),\(j\)层公式,\(n=\max\{i,j\}\)
            \item[(3)] \(A=B\vee C\),其中\(B,C\)分别为\(i\),\(j\)层公式,\(n=\max\{i,j\}\)
            \item[(4)] \(A=B\to C\),其中\(B,C\)分别为\(i\),\(j\)层公式,\(n=\max\{i,j\}\)
            \item[(5)] \(A=B\leftrightarrow C\),其中\(B,C\)分别为\(i\),\(j\)层公式,\(n=\max\{i,j\}\)
        \end{theitem}
        \item[3.] 若公式\(A\)的层次为\(k\),则称\(A\)是\(k\)层公式
    \end{theitem}
\end{itementry}

\begin{itementry}
    赋值/解释:设\(p_1,\dots,p_n\)是出现在公式\(A\)中的全部命题变项,给\(p_1,\dots,p_n\)各指定一个真值,称为对\(A\)的一个赋值或解释.若指定的一组值使\(A\)为\(1\),则称这组值为\(A\)的成真赋值.若使\(A\)为\(0\),则称这组值为\(A\)的成假赋值
\end{itementry}

\begin{itementry}
    真值表:将命题公式\(A\)在所有赋值下取值情况列成表,称为\(A\)的真值表
\end{itementry}

\begin{itementry}
    永真式\&永假式\&可满足式:设\(A\)为命题公式
    \begin{theitem}
        \item 若\(A\)在它的各种赋值下取值均为真,则称\(A\)为重言式或永真式或逻辑有效式
        \item 若\(A\)在它的各种赋值下取值均为假,则称\(A\)为矛盾式或永假式
        \item 若\(A\)至少存在一个成真赋值,则称\(A\)为可满足式
    \end{theitem}
\end{itementry}

\begin{itementry}
    哑元:和\(A\)取值无关的命题变项称为\(A\)的哑元
\end{itementry}

\chapter{命题逻辑等值演算}

\section{等值式}

\begin{itementry}
    等值:设\(A,B\)是两个命题公式,若\(A\),\(B\)构成的等价式\(A\leftrightarrow B\)为重言式,则称\(A\)与\(B\)是等值的,记为\(A\Leftrightarrow B\)
    \begin{subentry}
        特别地,\(\Leftrightarrow\)不是联结词
    \end{subentry}
\end{itementry}

\begin{itementry}
    定理:设\(A\)是一个命题公式,含有命题变项\(p-1,\dots,p_n\),又设\(A_1,\dots,A_n\)是任意的命题公式,对每一个\(i\),把\(p_i\)在\(A\)中所有出现都一换成\(A_i\),所得到的新命题公式记作\(B\),则若\(A\)是重言式,那么\(B\)也是重言式
\end{itementry}

\begin{itementry}
    等值式模式:
    \begin{theitem}
        \item 双重否定律:\(A\Leftrightarrow \neg\neg A\)
        \item 等幂律:\(A\Leftrightarrow A\vee A;A\Leftrightarrow A\wedge A\)
        \item 交换律:\(A\vee B\Leftrightarrow B\vee A,A\wedge B\Leftrightarrow B\wedge A\)
        \item 结合律:\(\begin{aligned}[t](A\vee B)\vee C\Leftrightarrow A\vee(B\vee C)\\(A\wedge B)\wedge C\Leftrightarrow A\wedge(B\wedge C)\end{aligned}\)
        \item 分配律:\(\begin{aligned}[t]A\vee(B\wedge C)\Leftrightarrow(A\vee B)\wedge(A\vee C)\\A\wedge(B\vee C)\Leftrightarrow(A\wedge B)\vee(A\wedge C)\end{aligned}\)
        \item 德摩根律:\(\begin{aligned}[t]\neg(A\vee B)\Leftrightarrow\neg A\wedge\neg B\\\neg(A\wedge B)\Leftrightarrow\neg A\vee\neg B\end{aligned}\)
        \item 吸收律:\(A\vee(A\wedge B)\Leftrightarrow A;A\wedge(A\vee B)\Leftrightarrow A\)
        \item 零律:\(A\vee 1\Leftrightarrow 1;A\wedge 0\Leftrightarrow 0\)
        \item 同一律:\(A\vee 0\Leftrightarrow 1;A\wedge 1\Leftrightarrow A\)
        \iitem 排中律:\(A\vee\neg A\Leftrightarrow 1\)
        \iitem 矛盾律:\(A\wedge\neg A\Leftrightarrow 0\)
        \iitem 蕴含等值式:\(A\to B\Leftrightarrow\neg A\vee B\)
        \iitem 等价等值式:\(A\leftrightarrow B\Leftrightarrow(A\to B)\wedge(B\to A)\)
        \iitem 假言易位:\(A\to B\Leftrightarrow\neg B\to\neg A\)
        \iitem 等价否定等值式:\(A\leftrightarrow B\Leftrightarrow\neg A\leftrightarrow\neg B\)
        \iitem 归谬论:\((A\to B)\wedge(A\to\neg B)\Leftrightarrow\neg A\)
    \end{theitem}
\end{itementry}

\begin{itementry}
    等值演算:由已知等值式推出另一些等值式的过程称为等值演算
\end{itementry}

\begin{itementry}
    置换规则:设\(\varPhi(A)\)是含公式\(A\)的命题公式,\(\varPhi(B)\)是用公式\(B\)置换\(\varPhi(A)\)中所有\(A\)的所有出现后得到的命题公式.若有\(B\Leftrightarrow A\),则有\(\varPhi(A)\Leftrightarrow\varPhi(B)\)
\end{itementry}

\section{析取范式与合取范式}

\begin{itementry}
    文字:命题变项及其否定统称为文字
\end{itementry}

\begin{itementry}
    简单析取式:仅有有限个文字构成的析取式
\end{itementry}

\begin{itementry}
    简单合取式:仅有有限个文字构成的合取式
\end{itementry}

\begin{itementry}
    定理:一个简单析取式是重言式当且仅当它同时包含某个命题变项及它的否定式;一个简单合取式是矛盾式当且仅当它同时含某个命题变项及它的否定式
\end{itementry}

\begin{itementry}
    析取范式:由有限个合取式的析取构成的命题公式称为析取范式,其一般形式为\(A_1\vee\cdots\vee A_s\),其中,\(A_i(i=1,\dots,s)\)为简单合取式
\end{itementry}

\begin{itementry}
    合取范式:由有限个析取式的合取构成的命题公式称为合取范式,其一般形式为\(A_1\wedge\cdots\wedge A_s\),其中\(A_i(i=1,\dots,s)\)为简单合取式
    \begin{subentry}
        特别地,\(p\vee\neg q\vee r\)既可以视为由三个简单合取式构成的析取范式,也可以视为一个简单析取式
    \end{subentry}
\end{itementry}

\begin{itementry}
    定理:一个析取范式是矛盾式当且仅当它的每个简单合取式都是矛盾式;一个合取范式是重言式当且仅当它的每个简单析取式都是重言式
\end{itementry}

\begin{itementry}
    范式存在定理:任一命题公式都存在与之等值的析取范式与合取范式
\end{itementry}

\begin{itementry}
    极小项(极大项):在含有\(n\)个命题变项的简单合取式(简单析取式)中,若每个命题变项和它的否定式恰好出现一次且仅出现一次,且命题变项或其否定式按照下表或字典排序,则称这样的简单合取式(简单析取式)为极小项(极大项)
    \begin{subentry}
        特别地,\(n\)个命题变项共可以产生\(2^{n}\)个极小项(极大项).每个极小项仅有一个成真赋值,每个极大项仅有一个成假赋值.若极小项(极大项)的成真赋值(成假赋值)所对应的二进制数等于十进制数\(i\),就将这个极小项(极大项)记作\(m_i\)\((M_i)\)
    \end{subentry}
\end{itementry}

\begin{itementry}
    定理:设\(m_i\)和\(M_i\)是命题变项含\(p_1,\dots,p_n\)的极小项和极大项,则\(\neg m_i\Leftrightarrow M_i\)
\end{itementry}

\begin{itementry}
    主析取范式(主合取范式):所有简单合取式(简单析取式)都是极小项(极大项)的析取范式(合取范式)(每个合取式/析取式所含命题变项的数量及种类需相同)
\end{itementry}

\begin{itementry}
    定理:任何命题公式都存在与之等值的主析取范式和主合取范式,并且是唯一的
\end{itementry}

\section{联结词的完备集}

\begin{itementry}
    \(n\)元真值函数:称\(F:\{0,1\}^n\to\{0,1\}\)为\(n\)元真值函数,其中,\hspace*{-0.5em}\\\(F\)的自变量为\(n\)个命题变项,定义域\(\{0,1\}^n=\{0\dots 0,\*0\dots 1,\*1\dots 1\}\),值域为\(\{0,1\}\)
\end{itementry}

\begin{itementry}
    联结词完备集:设\(S\)是一个联结词集合,若任何\(n(n\geq 1)\)元真值函数都可以仅由\(S\)中的联结词构成的公式表示,则称\(S\)是联结词完备集
\end{itementry}

\begin{itementry}
    与非:设\(p,q\)是两个命题,复合命题``\(p\)与\(q\)的否定式''称为\(p,q\)的与非式,记为\(p\uparrow q\),即\(p\uparrow q\Leftrightarrow\neg(p\wedge q)\).符号\(\uparrow\)称为与非联结词
\end{itementry}

\begin{itementry}
    或非:设\(p,q\)是两个命题,复合命题``\(p\)或\(q\)的否定式''称为\(p,q\)的或非式,记为\(p\downarrow q\),即\(p\downarrow q\Leftrightarrow\neg(p\vee q)\).符号\(\downarrow\)称为或非联结词
\end{itementry}

\begin{itementry}
    定理:\(S=\{\neg,\wedge,\vee\}\)是联结词完备集\\
    推论:以下联结词集都是联结词完备集:
    \begin{theitem}
        \item \(S_1=\{\neg,\wedge,\vee,\to\}\)
        \item \(S_2=\{\neg\wedge,\vee,\to,\leftrightarrow\}\)
        \item \(S_3=\{\neg,\wedge\}\)
        \item \(S_4=\{\neg,\vee\}\)
        \item \(S_5=\{\neg,\to\}\)
        \item \(S_6=\{\uparrow\}\)
        \item \(S_7=\{\downarrow\}\)
    \end{theitem}
\end{itementry}

\section{可满足性问题与消解法}

\begin{itementry}
    空简单析取式:不含任何文字的简单析取式,记为\(\lambda\),且空简单析取式不可满足
\end{itementry}

\begin{itementry}
    补:设\(l\)是文字,记\(l^c=\begin{cases}\neg p&\text{if}\,l=p\\p&\text{if}\, l=\neg p\end{cases}\),称为文字\(l\)的补
\end{itementry}

\begin{itementry}
    消解法:设\(C_1,C_2\)是两个简单析取式,\(C_1\)含文字\(l\),\(C_2\)含文字\(l^c\).从\(C_1\)中删去\(l\),从\(C_2\)中删去\(l^c\),然后将结果析取称一个简单析取式,称这样得到的简单式为\(C_1,C_2\)的(以\(l\)和\(l^c\)为消解文字的)消解式或消解结果,记为\(\Res(C_1,C_2)\).即设\(C_1=C_1'\vee l,C_2=C_2'\vee l^c\),\(\Res(C_1,C_2)=C_1'\vee C_2'\).由\(C_1,C_2\)得到\(\Res(C_1,C_2)\)的规则称为消解规则
\end{itementry}

\begin{itementry}
    定理:\(C_1\wedge C_2\approx\Res(C_1,C_2)\)(\(A\approx B\)表示\(A\)是可满足的当且仅当\(B\)是可满足的,\(C_1\)和\(C_2\)具有相同的可满足性,但它们不一定等值)
\end{itementry}

\begin{itementry}
    消解序列:设\(S\)是一个合取范式,\(C_1,\dots,C_n\)是一个简单析取式序列,若对每一个\(i(1\leq i\leq n)\),\(C_i\)是\(S\)中的一个简单析取式或\(C_i\)是它之前的两个简单析取式\(C_j,C_k\)\((1\leq j\leq k\leq i)\)的消解结果,则称此序列是由\(S\)导出\(C_n\)的消解序列.当\(C_n=\lambda\)时,称此序列是\(S\)的一个否证
\end{itementry}

\begin{itementry}
    消解的完全性:如果合取范式\(S\)有否证当且仅当\(S\)是不可满足的
\end{itementry}

\chapter{命题逻辑的推理理论}

\section{推理的形式结构}

\begin{itementry}
    推理:从前提出发推出结论的思维过程,设前提为集合\(\Gamma\),将由\(\Gamma\)推出\(B\)的推理记为\(\Gamma\vdash B\).若推理为正确的,则记为\(\Gamma\vDash B\),否则记为\(\Gamma\nvDash B\).这里称\(\Gamma\vdash B\)或\(\{A_1,\dots,A_k\}\vdash B\)为推理的形式结构
\end{itementry}

\begin{itementry}
    前提:已知的命题公式
\end{itementry}

\begin{itementry}
    结论:从前提出发应用推理规则推出的命题公式
\end{itementry}

\begin{itementry}
    有效/正确:设\(A_1,\dots,A_k\)和\(B\)都是命题公式,若对于\(A_1,\*\dots,\*A_k\)和\(B\)中出现的任意命题变项的任意一组赋值,或者\(A_1\wedge\cdots\wedge A_k\)为假,或者当\(A_1\wedge\cdots\wedge A_k\)为真时\(B\)也为真,则称由前提\(A_1,\dots,A_k\)推出结论\(B\)的推理时有效的或正确的,并称\(B\)为有效的结论
\end{itementry}

\begin{itementry}
    定理:命题公式\(A_1,\dots,A_k\)推出\(B\)的推理正确当且仅当\(A\wedge\cdots\wedge A_k\to B\)为重言式.
    \begin{subentry}
        即\(\{A_1,\dots,A_k\}\vDash B\)等价于\(A_1\wedge\cdots\wedge A_k\Rightarrow B\)
    \end{subentry}
\end{itementry}

\begin{itementry}
    推理定律:
    \begin{theitem}
        \item 附加律:\(A\Rightarrow(A\vee B)\)\label{logic:fujialv}
        \item 化简律:\((A\wedge B)\Rightarrow A\)
        \item 假言推理:\((A\to B)\wedge A\Rightarrow B\)
        \item 拒取式:\((A\to B)\wedge\neg B\Rightarrow\neg A\)
        \item 析取三段论:\((A\vee B)\wedge B\Rightarrow\neg A\)
        \item 假言三段论:\((A\to B)\wedge(B\to C)\Rightarrow(A\to C)\)
        \item 等价三段论:\((A\leftrightarrow B)\wedge(B\leftrightarrow C)\rightarrow(A\leftrightarrow C)\)
        \item 构造性二难:\((A\to B)\wedge(C\to D)\wedge(A\vee C)\Rightarrow (B\vee D)\)
        \item 构造性二难(特殊):\((A\to B)\wedge(\neg A\to B)\Rightarrow B\)
        \iitem 破坏性二难:
        \begin{align*}
            (A\to B)\wedge(C\to D)\wedge(\neg B\vee\neg D)\Rightarrow(\neg A\vee \neg C)
        \end{align*}
    \end{theitem}
\end{itementry}

\section{自然推理系统P}

\begin{itementry}
    形式系统\(I\):一个形式系统\(I\)由四部分组成:
    \begin{theitem}
        \item 非空字母表\(A(I)\)
        \item \(A(I)\)中符号构成的合式公式集\(E(I)\)
        \item \(E(I)\)中一些特殊的公式组成的公理集\(A_x(I)\)
        \item 推理规则集\(R(I)\)
    \end{theitem}
    将\(I\)记为4元组\(\left<A(I),E(I),A_x(I),R(I)\right>\).其中\(\left<A(I),E(I)\right>\)是\(I\)的形式语言系统,\(\left<A_x(I),R(I)\right>\)是\(I\)的形式演算系统
\end{itementry}

\begin{itementry}
    自然推理系统:从给定的前提出发,应用系统中的推理规则进行推理盐酸,最后得到的命题公式是推理的推论(它是有效的结论,可能是重言式,也可能不是重言式)
\end{itementry}

\begin{itementry}
    公理推理系统:从若干条给定的公理出发,应用系统中的推理规则进行推理盐酸,得到的结论是系统中的重言式,称为系统中的定理
\end{itementry}

\begin{itementry}
    证明:设前提\(A_1,\dots,A_k\)结论\(B\)和公式序列\(C_1,\dots,C_k\),若每一个\(i\),\(C_i\)是某个\(A_j\)或可由序列中前面的公式应用推理规则得到,且\(C_l=B\),那么称公式序列\(C_1,\dots,C_l\)是由\(A_1\dots,A_k\)推出\(B\)的证明
\end{itementry}

\begin{itementry}
    证明的方法:
    \begin{theitem}
        \item 附加前提证明法:若推理的形式如下:\((A_1\wedge\cdots\wedge A_k)\to(A\to B)\),其结论也为蕴含式,则可将结论中的前件作为推理的前提,使结论为\(B\),使\((A_1\wedge\cdots\wedge A_k)\to(A\to B)\Leftrightarrow(A_1\wedge\cdots\wedge A_k\wedge A)\to B\)
        \item 归谬法/反证法:在构造形式为\((A_1\wedge\cdots\wedge A_k)\to B\)的推理证明中,将\(\neg B\)作为前提能推出矛盾来,即证明\((A_1\wedge\cdots\wedge A_k\wedge\neg B)\)为矛盾式 
    \end{theitem}
\end{itementry}

\section{消解证明法}

\begin{itementry}
    消解证明法:把前提中的公式(和结论的否定)都化成等值的合取范式,以这些合取式中的所有简单析取式为前提,应用消解规则构造证明.若能得到空式,则证明推理是正确的
\end{itementry}

\chapter{一阶逻辑基本概念}

\section{一阶逻辑命题符号化}

\begin{itementry}
    个体词:研究对象中可独立存在的具体的或抽象的客体
\end{itementry}

\begin{itementry}
    个体常项:表示具体或特定的客体的个体词,一般用小写字母\(a,b,c\)表示
\end{itementry}

\begin{itementry}
    个体变项:表示抽象或泛指的个体词,常用\(x,y,z\)表示
\end{itementry}

\begin{itementry}
    个体域/论域\&全总个体域:个体变项的取值范围.由宇宙间一切事物组成的个体域称为全总个体域
\end{itementry}

\begin{itementry}
    谓词:用来刻画个体词性质及个体词之间关系的词,常用\(F,G,H\)表示
\end{itementry}

\begin{itementry}
    谓词常项:表示具体性质或关系的谓词
\end{itementry}

\begin{itementry}
    谓词变项:表示抽象或泛指的性质或关系的谓词.
    \begin{subentry}
        无论使谓词常项还是谓词变项,一般都记为\(F,G,H\)
    \end{subentry}
\end{itementry}

\begin{itementry}
    \(n\)元谓词:含\(n(n\geq 1)\)个个体变项\(x_1,\dots,x_n\)的谓词\(P\)称为\(n\)元谓词,记作\(P(x_1,\dots,x_n)\).\(n\)元谓词是以个体域为定义域,以\(\{0,1\}\)为值域的\(n\)元函数或关系
\end{itementry}

\begin{itementry}
    \(0\)元谓词:将不含个体变项的谓词称为0元谓词.
    \begin{subentry}
        特别地,当\(F,G,H\)为谓词常项时,\(0\)元谓词为命题
    \end{subentry}
\end{itementry}

\begin{itementry}
    存在量词:``存在'',``有一个''等词统称作存在量词,用``\(\exists\)''表示
\end{itementry}

\section{一阶逻辑公式及其解释}

\begin{itementry}
    一阶语言:用于一阶逻辑的形式语言
\end{itementry}

\begin{itementry}
    一阶逻辑:建立在一阶语言上的逻辑体系
\end{itementry}

\begin{itementry}
    非逻辑符号:个体常项符号,含舒服啊后,谓词符号
\end{itementry}

\begin{itementry}
    逻辑符号:个体变项符号,量词符号,联结词符号,括号,逗号
\end{itementry}

\begin{itementry}
    \(L\)生成的\(\mathscr{L}\):设\(L\)是非逻辑符号集,则由\(L\)生成的\(\mathscr{L}\)字母表包括:\par
    非逻辑符号:
    \begin{theitem}
        \item \(L\)中的个体常项符号,常用\(a,b,c\)表示
        \item \(L\)中的函数符号,常用\(f,g,h\)表示
        \item \(L\)中的谓词符号,常用\(F,G,H\)表示
    \end{theitem}
    逻辑符号
    \begin{theitem}
        \item 个体变项符号,常用\(x,y,z\)表示
        \item 量词符号:\(\forall,\exists\)
        \item 联结词符号:\(\neg,\wedge,\vee,\to,\leftrightarrow\)
        \item 括号与逗号:\((,),\hspace{0.5em},\)
    \end{theitem}
\end{itementry}

\begin{itementry}
    字母表\(\mathscr{L}\)的项:
    \begin{theitem}
        \item 个体常项符号和个体变项符号是项
        \item 若\(\varphi(x_1,\dots,x_n)\)是\(n\)元函数符号,\(t_1,\dots,t_n\)是\(n\)个项,则\(\varphi(t_1,\*\dots,t_n)\)是项
        \item 所有项都是有限次使用1.2.得到的
    \end{theitem}
\end{itementry}

\begin{itementry}
    原子公式:设\(R(x_1,\dots,x_n)\)是\(\mathscr{L}\)的\(n\)元谓词符号,\(t_1,\dots,t_n\)是\(\mathscr{L}\)\*的\(n\)个项,则称\(R(t_1,\dots,t_n)\)是\(\mathscr{L}\)的原子公式
\end{itementry}

\begin{itementry}
    \(\mathscr{L}\)的合式公式/谓词公式/公式:
    \begin{theitem}
        \item 原子公式是合式公式
        \item 若\(A\)是合式公式,则\(\neg A\)也是合式公式
        \item 若\(A,B\)是合式公式,则\(A\wedge B,A\vee B,A\to B,A\leftrightarrow B\)也是合式公式
        \item 若\(A\)是合式公式,则\(\forall xA,\exists xA\)也是合式公式
        \item 有限次使用1.-4.构成的符号串是合式公式
    \end{theitem}
\end{itementry}

\begin{itementry}
    指导变元\&辖域:在公式\(\forall xA,\exists xA\)中,\(x\)称为指导变元,\(A\)称为量词的辖域
\end{itementry}

\begin{itementry}
    约束出现\&自由出现:在\(\forall x\)和\(\exists x\)的辖域中,\(x\)的所有出现都称为约束出现,\(A\)中不是约束出现的其他变项均称做自由出现
\end{itementry}

\begin{itementry}
    封闭的公式/闭式:设\(A\)是任意公式,若\(A\)中不含自由出现的个体变项,则称\(A\)为封闭的公式,简称闭式
\end{itementry}

\begin{itementry}
    解释:对公式中个体及个体常项符号,函数符号,谓词符号的制定称为解释
\end{itementry}

\begin{itementry}
    赋值:指定自由出现的个体变项的值称为赋值
\end{itementry}

\begin{itementry}
    解释:设\(\mathscr{L}\)是\(L\)生成的一阶语言,则\(\mathscr{L}\)的解释包括:
    \begin{theitem}
        \item 非空个体域\(D_I\)
        \item 对每一个个体常项符号\(a\in L\),有一个\(\overline{a}\in D_I\),称\(\overline{a}\)为\(a\)在\(I\)中的解释
        \item 对每一个\(n\)元函数符号\(f\in L\),有一个\(D_I\)上的\(n\)元函数\(\overline{f}:D_I^n\to D_I\),称\(\overline{f}\)为\(f\)在\(I\)中的解释
        \item 对每一个\(n\)元谓词符号\(F\in L\),有一个\(D_I\)上的\(n\)元谓词常项\(\overline{F}\),称\(\overline{F}\)为\(F\)在\(I\)中的解释
    \end{theitem}
\end{itementry}

\begin{itementry}
    赋值:对每一个个体变项符号\(x\)指定\(D_I\)中的一个值\(\sigma(x)\)的过程称为赋值
\end{itementry}

\begin{itementry}
    \(A\)在\(I\)下的解释:设有公式\(A\),在解释\(I\)和赋值\(\sigma\)下
    \begin{theitem}
        \item 取个体域\(D_I\)
        \item 若\(A\)中含个体符号\(a\),则将其替换为\(\overline{a}\)
        \item 若\(A\)中含函数符号\(f\),则将其替换为\(\overline{f}\)
        \item 若\(A\)中含谓词符号\(F\),则将其替换为\(\overline{F}\)
        \item 若\(A\)中含自由出现的\(x\),则将其换成\(\sigma(x)\)
    \end{theitem}
    把这样得到的公式记为\(A'\),称\(A'\)为\(A\)在\(I\)下的解释,或称\(A\)在\(I\)下被解释为\(A'\)
\end{itementry}

\begin{itementry}
    代换实例:设\(A_0\)是含命题变项\(p_1,\dots,p_n\)的命题公式,\(A_1,\dots,A_n\)是\(n\)个谓词公式,用\(A_i\)处处代替\(A_0\)中的\(p_i\)所得到的公式\(A\)称为\(A_0\)的代换实例
\end{itementry}

\begin{itementry}
    定理:重言式的代换实例都是重言式,矛盾式的代换实例都是矛盾式
\end{itementry}

\chapter{一阶逻辑等值演算与推理}

\section{一阶逻辑等值式与置换规则}

\begin{itementry}
    常见等值式:
    \begin{theitem}
        \item 消去量词等值式:设个体域为有限集\(D=\{a_1,\dots,a_n\}\),则
        \begin{theitem}
            \item[(1)] \(\forall xA(x)\Leftrightarrow A(a_1)\wedge A(a_2)\wedge\cdots\wedge A(a_n)\)
            \item[(2)] \(\exists xA(x)\Leftrightarrow A(a_1)\vee A(a_2)\vee\cdots\vee A(a_n)\)
        \end{theitem}
        \item[2.] 量词否定等值式:设公式\(A(x)\)含自由出现的\(x\),则
        \begin{theitem}
            \item[(1)] \(\neg\forall xA(x)\Leftrightarrow\exists x\neg A(x)\)
            \item[(2)] \(\neg\exists xA(x)\Leftrightarrow\forall x\neg A(x)\) 
        \end{theitem}
        \item[3.] 量词辖域收缩与扩张等值式:设公式\(A(x)\)含自由出现的个体变项\(x\),\(B\)不含自由出现的\(x\),那么就有
        \begin{theitem}
            \item[(1)] 
            \(\begin{aligned}[t]
                &\forall x(A(x)\vee B)\Leftrightarrow \forall xA(x)\vee B\\
                &\forall(A(x)\wedge B)\Leftrightarrow\forall xA(x)\wedge B\\
                &\forall x(A(x)\to B)\Leftrightarrow\exists xA(x)\to B\\
                &\forall x(B\to A(x))\Leftrightarrow B\to\forall xA(x)
            \end{aligned}\)
            \item[(2)] 
            \(\begin{aligned}[t]
                &\exists x(A(x)\vee B)\Leftrightarrow\exists xA(x)\vee B\\
                &\exists x(A(x)\wedge B)\Leftrightarrow\exists xA(x)\wedge B\\
                &\exists x(A(x)\to B)\Leftrightarrow\forall xA(x)\to B\\
                &\exists (B\to A(x))\Leftrightarrow B\to\exists A(x)
            \end{aligned}\)
        \end{theitem}
        \item[4.] 量词分配等值式:设公式\(A(x),B(x)\)含自由出现的个体变项\(x\),那么就有:
        \begin{theitem}
            \item \(\forall x(A(x)\wedge B(x))\Leftrightarrow\forall xA(x)\wedge\forall xB(x)\)
            \item \(\exists x(A(x)\vee B(x))\Leftrightarrow\exists xA(x)\vee\exists xB(x)\)
            \item \(\forall x(A(x)\vee B(x))\nLeftrightarrow\forall xA(x)\vee \forall xB(x)\)
            \item \(\exists x(A(x)\wedge B(x))\nLeftrightarrow\exists xA(x)\wedge\exists xB(x)\)
        \end{theitem}
    \end{theitem}
\end{itementry}

\begin{itementry}
    置换规则:设\(\varPhi(A)\)是含公式\(A\)的公式,\(\varPhi(B)\)是用公式\(B\)取代\(\varPhi(A)\)中所有的\(A\)之后所得到的公式,则若\(A\Leftrightarrow B\),则\(\varPhi(A)\Leftrightarrow\varPhi(B)\)
\end{itementry}

\begin{itementry}
    换名规则:设\(A\)为一公式,将\(A\)中某量词辖域中的一个约束变项的所有出现及相应的指导变元全部改成该量词辖域中未曾出现过的某个个体变项的符号,所得到的公式记为\(A'\),则\(A'\Leftrightarrow A\)
\end{itementry}

\section{一阶逻辑前束范式}

\begin{itementry}
    前束范式:具有形式\(Q_1x_1\dots Q_kx_kB\)的一阶逻辑公式称为前束范式,其中\(Q_i\)为量词,\(B\)为不含量词的公式
\end{itementry}

\begin{itementry}
    前束范式存在定理:一阶逻辑中的任何公式都存在等值的前束范式
\end{itementry}

\begin{itementry}
    常见的等值式:
    \begin{theitem}
        \item 
        \(\begin{aligned}[t]
            &\neg\exists x(M(x)\wedge F(x))\\
            \Leftrightarrow&\forall x(M(x)\to\neg F(x))
        \end{aligned}\)
        \item 
        \(\begin{aligned}[t]
            &\neg\forall x(M(x)\to F(x))\\
            \Leftrightarrow&\exists x(M(x)\wedge\neg F(x))
        \end{aligned}\)
        \item 
        \(\begin{aligned}[t]
            &\neg\forall x\forall y(F(x)\wedge G(y)\to H(x,y))\\
            \Leftrightarrow&\exists x\exists y(F(x)\wedge G(y)\wedge\neg H(x,y))
        \end{aligned}\)
        \item 
        \(\begin{aligned}[t]
            &\neg\exists x\exists y(F(x)\wedge G(y)\wedge L(x,y))\\
            \Leftrightarrow&\forall x\forall y(F(x)\wedge G(y)\to\neg L(x,y))
        \end{aligned}\)
    \end{theitem}
\end{itementry}

\section{一阶逻辑的推理理论}

\begin{itementry}
    重要的推理定律
    \begin{theitem}
        \item \(\forall xA(x)\vee\forall xB(x)\Rightarrow x(A(x)\vee B(x))\)
        \item \(\exists x(A(x)\wedge B(x))\Rightarrow \exists xA(x)\wedge\exists x(B(x))\)
        \item \(\forall x(A(x)\to B(x))\Rightarrow \forall xA(x)\to\forall x(B(x))\)
        \item \(\exists x(A(x)\to B(x))\Rightarrow\exists xA(x)\to\exists x(B(x))\)
    \end{theitem}
\end{itementry}

\begin{itementry}
    量词引入与消去规则:设前提\(\varGamma=\{A_1,\dots,A_k\}\)
    \begin{theitem}
        \item 全称量词消去规则(简记为\(\forall -\))\par
        \(\forall xA(x)\Rightarrow A(y)\)或\(\forall xA(x)\Rightarrow A(c)\),其中\(x,y\)是个体变项符号,\(c\)是个体常项符号,且\(A\)中\(x\)不在\(\forall y\)和\(\exists y\)的辖域出现
        \item 全称量词引入规则(简记为\(\forall +\))\par
        \(A(y)\Rightarrow\forall xA(x)\),其中\(y\)是个体变项符号,且不在\(\varGamma\)的任何公式中自由出现\par
        即为了证明\(\forall xA(x)\)为真,只需证明任取一个\(y\),\(A(y)\)为真
        \item 存在量词消去规则(简记为\(\exists -\))\par
        \(\exists xA(x)\wedge(A(y)\to B)\Rightarrow B\)或\(A(y)\to B\Rightarrow\exists xA(x)\to B\).\(\exists xA(x)\wedge A(c)\to B\Rightarrow B\)或\(A(c)\to B\Rightarrow\exists xA(x)\to B\).其中\(y\)是个体变项符号,且不在\(\varGamma\)的任何公式和\(B\)中自由出现,\(c\)是个体常项,且不在\(\varGamma\)的任何公式和\(A,B\)中出现
        \item 存在量词引入规则(简记为\(\exists +\))\par
        \(A(y)\Rightarrow\exists xA(x)\)或\(B\to A(y)\Rightarrow B\to\exists xA(x)\).\(A(c)\Rightarrow\exists xA(x)\)或\(B\to A(c)\Rightarrow\exists xA(x)\).其中\(x,y\)是个体变项符号,\(c\)是个体常项符号,且在\(A\)中\(y,c\)分别不在\(\forall x,\exists x\)的辖域内自由出现
    \end{theitem}
\end{itementry}

\begin{itementry}
    一阶逻辑自然推理系统\(N_{\mathscr{L}}\):自然推理系统\(N_{\mathscr{L}}\)包含:
    \begin{theitem}
        \item 字母表:同一阶语言\(\mathscr{L}\)的字母表
        \item 合式公式:同一阶语言\(\mathscr{L}\)的合式公式
        \item 推理规则:
        \begin{theitem}
            \item[(1)] 前提引入规则:在证明的任何步骤都可以引入前提
            \item[(2)] 结论引入规则:在证明的任何步骤所得到的结论都可以作为后继证明的前提
            \item[(3)] 置换规则:在证明的任何步骤,命题公式中的子公式都可以用等值的公式替换,得到公式序列中的另一个公式
            \item[(4)] 假言推理规则/分离规则:\(A\to B\wedge A\Rightarrow B\)
            \item[(5)] 附加规则\hspace{2em}见\hyperref[logic:fujialv]{\(P_{\pageref{logic:fujialv}}\)}
            \item[(6)] 化简规则
            \item[(7)] 拒取式规则
            \item[(8)] 假言三段论规则
            \item[(9)] 析取三段论规则
            \item[]\hspace{-1.3em}(10)构造性二难推理规则
            \item[]\hspace{-1.3em}(11)合取引入规则
            \item[]\hspace{-1.3em}(12)\(\forall-\)规则
            \item[]\hspace{-1.3em}(13)\(\forall+\)规则
            \item[]\hspace{-1.3em}(14)\(\exists-\)规则
            \item[]\hspace{-1.3em}(15)\(\exists+\)规则
        \end{theitem}
    \end{theitem}
\end{itementry}